x:chain_config(). (ccsucc?(x))  (ccsucc-num(x)  ) 

latex

Definitions	s = t, t  T, True, x:AB(x), P  Q, Id, , chain config ind ccsucc compseq tag def, b, ccsucc?(x), ccsucc-num(x), False, chain config ind ccpred compseq tag def, chain config ind cctail compseq tag def, chain config ind cchead compseq tag def, x:A  B(x), left + right, , Unit, chain_config(), x:A. B(x)
Lemmas	nat wf, member wf, assert wf, chain config wf, false wf, true wf